package plp.imperative2.declaration;

import java.util.ArrayList;

import plp.expressions2.expression.ValorBooleano;
import plp.expressions2.memory.IdentificadorJaDeclaradoException;
import plp.expressions2.memory.IdentificadorNaoDeclaradoException;
import plp.imperative1.command.Comando;
import plp.imperative1.memory.AmbienteExecucaoImperativa;
import plp.imperative1.memory.EntradaVaziaException;
import plp.imperative2.memory.ContextoExecucaoImperativa2;
import plp.imperative2.memory.ContratoException;
import plp.imperative2.memory.DurException;
import plp.imperative2.memory.InvException;
import plp.imperative2.memory.PreCondicaoException;

public class DefProcedimentoDbc extends DefProcedimento {

	private DefPrePosDBC definicaoPrePos;

	private DefDurDbc expressao;

	private long duracaoExecucao;

	public DefProcedimentoDbc(ListaDeclaracaoParametro parametrosFormais,
			Comando comando) {
		super(parametrosFormais, comando);
	}

	public void setListaDefDbc(DefPrePosDBC dbc) {
		this.definicaoPrePos = dbc;
	}

	private void iniciarContadorDuracao() {
		duracaoExecucao = System.currentTimeMillis();
		System.out.println(System.currentTimeMillis());
	}

	private long finalizarContadorDuracao() {
		System.out.println(System.currentTimeMillis());
		return duracaoExecucao = System.currentTimeMillis() - duracaoExecucao;
	}

	public AmbienteExecucaoImperativa executar(
			AmbienteExecucaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, EntradaVaziaException,
			ContratoException {
		iniciarContadorDuracao();

		AmbienteExecucaoImperativa ambienteAux;

		executaPreCondicao(ambiente);

		executaInvariante(ambiente);

		ambienteAux = getComando().executar(ambiente);

		executaInvariante(ambiente);

		((ContextoExecucaoImperativa2) ambiente)
				.setTempoExecucao(finalizarContadorDuracao());

		executaPosCondicao(ambiente);

		return ambienteAux;
	}

	protected void executaPreCondicao(AmbienteExecucaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, PreCondicaoException,
			EntradaVaziaException, ContratoException {

		if (definicaoPrePos != null)
			definicaoPrePos.avaliarPre(ambiente);
	}

	protected void executaPosCondicao(AmbienteExecucaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, PreCondicaoException,
			EntradaVaziaException, ContratoException {
		if (definicaoPrePos != null)
			definicaoPrePos.avaliarPos(ambiente);
	}

	protected void executaInvariante(AmbienteExecucaoImperativa ambiente)
			throws IdentificadorJaDeclaradoException,
			IdentificadorNaoDeclaradoException, PreCondicaoException,
			EntradaVaziaException, ContratoException {

		ArrayList<DeclaracaoInvariante> invariantes = ((ContextoExecucaoImperativa2) ambiente)
				.getInvariantes();

		for (DeclaracaoInvariante invariante : invariantes) {
			ValorBooleano valorAvaliacao = (ValorBooleano) invariante
					.avaliar(ambiente);
			if ((valorAvaliacao).isEquals(new ValorBooleano(false))) {
				throw new InvException(invariante);
			}
		}

	}

}
